1  isprop(p)⊃iscond(mkcond(p,a,b))   --- ∀E condsyn0 p,a,b

2  s1(mkcond(p,a,b))=p   --- ∀E condsyn1 p,a,b

3  s2(mkcond(p,a,b))=a   --- ∀E condsyn2 p,a,b

4  isprop(p)⊃iscond(mkcond(p,a,c))   --- ∀E condsyn0 p,a,c

5  s1(mkcond(p,a,c))=p   --- ∀E condsyn1 p,a,c

6  s2(mkcond(p,a,c))=a   --- ∀E condsyn2 p,a,c

7  s3(mkcond(p,a,c))=c   --- ∀E condsyn3 p,a,c

8  isprop(p)⊃iscond(mkcond(p,mkcond(p,a,b),c))   --- ∀E condsyn0 p,mkcond(p,a,b),c

9  s1(mkcond(p,mkcond(p,a,b),c))=p   --- ∀E condsyn1 p,mkcond(p,a,b),c

10  s2(mkcond(p,mkcond(p,a,b),c))=mkcond(p,a,b)   --- ∀E condsyn2 p,mkcond(p,a,b),c

11  s3(mkcond(p,mkcond(p,a,b),c))=c   --- ∀E condsyn3 p,mkcond(p,a,b),c

12  (iscond(mkcond(p,a,b))∧value(s1(mkcond(p,a,b)))=T)⊃value(mkcond(p,a,b))=value(s2(mkcond(p,a,b)))   --- ∀E co~
ndval0 mkcond(p,a,b)

13  (iscond(mkcond(p,a,c))∧value(s1(mkcond(p,a,c)))=T)⊃value(mkcond(p,a,c))=value(s2(mkcond(p,a,c)))   --- ∀E co~
ndval0 mkcond(p,a,c)

14  (iscond(mkcond(p,a,c))∧value(s1(mkcond(p,a,c)))=F)⊃value(mkcond(p,a,c))=value(s3(mkcond(p,a,c)))   --- ∀E co~
ndval1 mkcond(p,a,c)

15  (iscond(mkcond(p,a,c))∧value(s1(mkcond(p,a,c)))=U)⊃value(mkcond(p,a,c))=U   --- ∀E condval2 mkcond(p,a,c)

16  (iscond(mkcond(p,mkcond(p,a,b),c))∧value(s1(mkcond(p,mkcond(p,a,b),c)))=T)⊃value(mkcond(p,mkcond(p,a,b),c))=~
value(s2(mkcond(p,mkcond(p,a,b),c)))   --- ∀E condval0 mkcond(p,mkcond(p,a,b),c)

17  (iscond(mkcond(p,mkcond(p,a,b),c))∧value(s1(mkcond(p,mkcond(p,a,b),c)))=F)⊃value(mkcond(p,mkcond(p,a,b),c))=~
value(s3(mkcond(p,mkcond(p,a,b),c)))   --- ∀E condval1 mkcond(p,mkcond(p,a,b),c)

18  (iscond(mkcond(p,mkcond(p,a,b),c))∧value(s1(mkcond(p,mkcond(p,a,b),c)))=U)⊃value(mkcond(p,mkcond(p,a,b),c))=~
U   --- ∀E condval2 mkcond(p,mkcond(p,a,b),c)

19  isprop(p)⊃(value(p)=T∨(value(p)=F∨value(p)=U))   --- ∀E condtri1 p

20  z=y⊃y=z   --- ∀E equal1 z,y

21  (x=y∧y=z)⊃x=z   --- ∀E equal2 x,y,z

22  (x=y∧z=y)⊃x=z   --- TAUT

23  ∀x y z.((x=y∧z=y)⊃x=z)   --- ∀I 22 z←z  y←y  x←x 

24  (value(mkcond(p,mkcond(p,a,b),c))=value(a)∧value(mkcond(p,a,c))=value(a))⊃value(mkcond(p,mkcond(p,a,b),c))=v~
alue(mkcond(p,a,c))   --- ∀E 23 value(mkcond(p,mkcond(p,a,b),c)),value(a),value(mkcond(p,a,c))

25  (value(mkcond(p,mkcond(p,a,b),c))=value(c)∧value(mkcond(p,a,c))=value(c))⊃value(mkcond(p,mkcond(p,a,b),c))=v~
alue(mkcond(p,a,c))   --- ∀E 23 value(mkcond(p,mkcond(p,a,b),c)),value(c),value(mkcond(p,a,c))

26  (value(mkcond(p,mkcond(p,a,b),c))=U∧value(mkcond(p,a,c))=U)⊃value(mkcond(p,mkcond(p,a,b),c))=value(mkcond(p,~
a,c))   --- ∀E 23 value(mkcond(p,mkcond(p,a,b),c)),U,value(mkcond(p,a,c))

27  (iscond(mkcond(p,a,b))∧value(p)=T)⊃value(mkcond(p,a,b))=value(s2(mkcond(p,a,b)))   --- SUBST2IN12

28  (iscond(mkcond(p,a,b))∧value(p)=T)⊃value(mkcond(p,a,b))=value(a)   --- SUBST3IN27

29  (iscond(mkcond(p,mkcond(p,a,b),c))∧value(p)=T)⊃value(mkcond(p,mkcond(p,a,b),c))=value(s2(mkcond(p,mkcond(p,a~
,b),c)))   --- SUBST9IN16

30  (iscond(mkcond(p,mkcond(p,a,b),c))∧value(p)=T)⊃value(mkcond(p,mkcond(p,a,b),c))=value(mkcond(p,a,b))   --- S~
UBST10IN29

31  (iscond(mkcond(p,a,c))∧value(p)=T)⊃value(mkcond(p,a,c))=value(s2(mkcond(p,a,c)))   --- SUBST5IN13

32  (iscond(mkcond(p,a,c))∧value(p)=T)⊃value(mkcond(p,a,c))=value(a)   --- SUBST6IN31

33  (iscond(mkcond(p,a,c))∧value(p)=F)⊃value(mkcond(p,a,c))=value(s3(mkcond(p,a,c)))   --- SUBST5IN14

34  (iscond(mkcond(p,a,c))∧value(p)=F)⊃value(mkcond(p,a,c))=value(c)   --- SUBST7IN33

35  (iscond(mkcond(p,mkcond(p,a,b),c))∧value(p)=F)⊃value(mkcond(p,mkcond(p,a,b),c))=value(s3(mkcond(p,mkcond(p,a~
,b),c)))   --- SUBST9IN17

36  (iscond(mkcond(p,mkcond(p,a,b),c))∧value(p)=F)⊃value(mkcond(p,mkcond(p,a,b),c))=value(c)   --- SUBST11IN35

37  (iscond(mkcond(p,a,c))∧value(p)=U)⊃value(mkcond(p,a,c))=U   --- SUBST5IN15

38  (iscond(mkcond(p,mkcond(p,a,b),c))∧value(p)=U)⊃value(mkcond(p,mkcond(p,a,b),c))=U   --- SUBST9IN18

39  (value(mkcond(p,mkcond(p,a,b),c))=value(mkcond(p,a,b))∧value(mkcond(p,a,b))=value(a))⊃value(mkcond(p,mkcond(~
p,a,b),c))=value(a)   --- ∀E equal2 value(mkcond(p,mkcond(p,a,b),c)),value(mkcond(p,a,b)),value(a)

40  isprop(p)⊃value(mkcond(p,mkcond(p,a,b),c))=value(mkcond(p,a,c))   --- TAUT

41  ∀p a b c.(isprop(p)⊃value(mkcond(p,mkcond(p,a,b),c))=value(mkcond(p,a,c)))   --- ∀I 40 c←c  b←b  a←a  p←p